Alive memory model - #1455

Co-authored-by: Luigi Rinaldi <82770895+luigirinaldi@users.noreply.github.com>

Co-authored-by: Luigi Rinaldi <82770895+luigirinaldi@users.noreply.github.com>

Co-authored-by: Luigi Rinaldi <82770895+luigirinaldi@users.noreply.github.com>

The interpreter's memory model is about to change substantially. This
adds the tool that checks it against a reference which already encodes
LLVM's rules for provenance, liveness, alignment and poison: random
memory-using programs are run under both `veir-interpret` and Alive2's
`alive-exec`, and the cases where they disagree are reported.

`Tools/memfuzz_generate.py` builds each program once and prints it
twice, as generic LLVM-dialect MLIR and as LLVM IR, so a difference in
the two answers is a difference in semantics rather than in a
translator. Its defaults track what the interpreter models, which
today is `alloca`, `getelementptr` and in-bounds integer loads and
stores; everything past that is behind an option, and each later
change to the model turns on the one it makes correct.

Work is split by seed rather than by distributing programs: case `n`
of a run is generated from the run identifier and `n` alone, so shard
`i` of a hundred covers a block no other shard touches and any case is
reproducible anywhere from its index. `farm` starts the shards over
ssh, through a SLURM array, or across local cores, and `collect`
merges the reports and ranks what turned up.

Verdicts separate real findings from the reference being imprecise: a
defined VeIR result that agrees bit for bit with an Alive2 poison is a
refinement, not a bug. `Test/Tools/memfuzz_smoke.mlir` exercises the
half that does not need alive-exec, so a generator that drifts from
the interpreter is caught by the ordinary test suite.

Memory was one flat byte array, so a pointer could walk from one
allocation into its neighbour and nothing distinguished allocations.
Memory is now an array of objects, one per allocation, and a pointer
is an object index with a 64-bit offset. Loads and stores are checked
against their own object by `MemoryState.checkAccess`, which is the
one place every later condition on an access is added.

Every object has a base address, assigned by a bump allocator that
honours the alignment its allocation declares, leaves a guard byte
between objects, and starts past a 64 KiB arena that machine code may
address directly. A pointer converts to an integer as base plus
offset, and an integer converts back by binary search over the bases,
so bitcasts, unrealized casts to registers and pointers stored in
memory keep their meaning. RISC-V accesses decode the register value
the same way and grow the object they land in up to the next object's
base, which keeps machine code that addresses memory freely working.

Memory refinement lifts from the flat array to the objects: the same
number of objects, each at the same address and refined bytewise.

The fuzzing harness gains the null-dereference knob this makes correct.
Deliberately undefined accesses stay off until the next change adds
alignment, since before it the two tools would disagree on misaligned
accesses for a reason unrelated to bounds.

Loads and stores now honour their `alignment` attribute: the physical
address of the access must be a multiple of it, else the access is
undefined behaviour. Without the attribute the natural alignment of the
accessed type, its size, applies, as LLVM does for accesses that carry
no explicit alignment. RISC-V accesses stay unaligned, as the hardware
allows.

The condition lives in `MemoryState.checkAccess` beside the bounds
check, and like it does not apply to an access of no bytes.

With both conditions an access can break in place, the harness turns
on deliberately undefined accesses, out-of-bounds offsets and
misaligned accesses together, aiming them at any object whose
provenance it knows.

A byte of memory is now either a value byte with its poison bits or one
of the eight fragments of a stored pointer. Storing a pointer writes
its fragments, and loading a pointer type yields the stored pointer
when all eight fragments are present in order, the pointer at the
stored address when the bytes are defined values, and a poison pointer
otherwise, which includes a run of fragments that was partly
overwritten. Integer loads over fragments read the pointer's physical
address, so pointers leak into integers through memory as in LLVM.
RISC-V stores write value bytes and RISC-V loads read addresses through
fragments.

The `ptrtoint` and `inttoptr` ops convert through the address space,
with poison mapping to poison in both directions, and
`llvm.intr.memcpy`, `memmove` and `memset` are interpreted. Copies move
bytes verbatim, so provenance survives, and `memcpy` requires its two
ranges to be equal or disjoint, which is the only thing separating it
from `memmove`. `memset` writes value bytes.

Memory refinement is defined per byte: value bytes refine as before, a
fully poison value byte is refined by anything, and a fragment only by
the same fragment. Objects must agree in address and size.

The harness gains the pointer-value and memory-intrinsic knobs this
makes correct, and takes address differences only from pointers whose
provenance it knows: from a poison pointer the difference is poison in
VeIR and zero in Alive2, which is a question about poison rather than
about memory.

An object now records how it was allocated, the alignment it was given,
whether it is still alive and whether it may be written. Two conditions
join the access check that every load and store already goes through:
an access of at least one byte must reach an object that is alive, and
a write must not target a constant object. An access of no bytes stays
allowed anywhere, even through a dangling pointer, as in Alive2.

Stack objects die at `llvm.intr.lifetime.end` and when the function
that allocated them returns; `llvm.intr.lifetime.start` revives one
with poison contents. Both marks name a whole object, so applying one
to anything but the start of a stack object is undefined behaviour.

The remaining kinds, heap and global, have no allocations yet; they
arrive with the operations that create them.

`llvm.call` now models the C and C++ allocation functions by name:
`malloc`, `calloc`, which zeroes, `realloc`, which copies and then
frees, `free`, and `operator new` and `delete` by their mangled names.
Each allocation is a fresh object, so pointers from different calls
never alias, and a freed object dies but keeps its address, which is
never reused, so a use after free is caught rather than landing in
whatever was allocated next. Freeing anything but a live heap object at
its start is undefined behaviour, which covers double frees and freeing
an `alloca`.

Whether an allocation fails is the model's first nondeterministic
choice, so it is drawn from an oracle carried in the memory state,
indexed by how many allocations came before. The default oracle never
fails, and two programs being compared are run against the same one.

A copy of no bytes now reaches no memory before its pointers are
inspected, matching the rule the access check already applies, so a
zero-length `memcpy` or `memset` is allowed through any pointer.

`veir-interpret` now materializes the module's globals as objects
before `main` runs. A global with a `value` attribute starts with its
bytes, integers little-endian and strings verbatim; one with an
initializer region starts with the value that region returns; anything
else starts as poison. A `constant` global becomes read-only once its
initializer has been stored, so writing to it is undefined behaviour.
Functions get empty objects of their own, so their addresses are
distinct from each other and from every allocation.

`llvm.mlir.addressof` looks a symbol up in the map from names to
objects that this builds, and yields a pointer to the start of one.

…utes

An object records whether its address escaped: stored to memory,
converted to an integer or to register bits, passed to a call, or
returned from a function. Globals are escaped from the start. Only
escaped objects can be reached by code the interpreter does not see.

A call to any function that is not one of the modelled allocation
functions is an unknown call, which the interpreter cannot enter. It
escapes its pointer arguments, then havocs every live, writable,
escaped object, replacing its bytes with what the oracle chooses, and
returns the oracle's value for each result, poison by default. Objects
that never escaped keep their contents across the call.

Argument attributes become undefined-behaviour conditions: `llvm.nonnull`
forbids null, `llvm.dereferenceable = n` demands `n` readable bytes at
the pointer, and `llvm.align = n` demands an address that is a multiple
of `n`. They are checked at every `llvm.call` and on entry to an
`llvm.func`, and a poison pointer satisfies none of them.

`FunctionResult.isRefinedBy` no longer demands equal final memories. It
is now relative to the memory the function started with and follows
Alive2: a renaming sends the target's objects to the source's, is the
identity on the objects that existed before the call, and sends objects
the target allocated to objects the source allocated. Every source
object the caller can observe, meaning it existed before the call or
its address escaped, must be refined by the target object the renaming
sends to it, with the same size and liveness, an escape matched by an
escape, and bytes refined pointwise where pointer fragments are related
through the renaming. Returned values refine under the renaming too,
with a poison pointer refined by any pointer. Objects the source
allocated but never leaked are unconstrained, so a transformation may
drop an allocation.

Reflexivity and transitivity are proved, the latter by composing the
two renamings, and `isRefinedByAsFunction` uses the new relation. A
bridge lemma shows that equal final memories with refining results
still refine, which is what proofs built on the state-level relation
provide. That relation and the monotonicity axiom keep memory equality,
since a single-operation rewrite does not change the memory.